Inference at * 1 1 1 1 1 
Iof proof for Lemma inv image ind tp:

.....assertion..... NILNIL

1. T : Type
2. r : TT
3. S : Type
4. f : ST
5. WellFnd{i}(T;x,y.r(x,y))
6. P : S
7. j:S. (k:S. r(f(k),f(j))  P(k))  P(j)
8. S
  x:T, n:S. (f(n) = x)  P(n) 

latex

 by (\p. 
 ((Thin (get_int_arg `i` p)) 
CollapseTHEN (D 0)) p) 

latex

C1: 

C1: 8. x : T
C1:   n:S. (f(n) = x)  P(n)
C2: .....wf..... NILNIL

C2: 7. j:S. (k:S. r(f(k),f(j))  P(k))  P(j)
C2:   T  Type
C.

Definitions

x:A. B(x), t  T